YES 1.719 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((isSuffixOf :: Eq a => [Maybe a ->  [Maybe a ->  Bool) :: Eq a => [Maybe a ->  [Maybe a ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] _ True
isPrefixOf [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((isSuffixOf :: Eq a => [Maybe a ->  [Maybe a ->  Bool) :: Eq a => [Maybe a ->  [Maybe a ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule List
  (isSuffixOf :: Eq a => [Maybe a ->  [Maybe a ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xy4000), Succ(xy2601000)) → new_primPlusNat(xy4000, xy2601000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xy23100), Succ(xy260100)) → new_primMulNat(xy23100, Succ(xy260100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy2300), Succ(xy26000)) → new_primEqNat(xy2300, xy26000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs2(Just(xy230), Just(xy2600), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs1(xy230, xy2600, bbb, bbc, bbd)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(ty_[], bdc)) → new_esEs(xy230, xy2600, bdc)
new_esEs(:(xy230, xy231), :(xy2600, xy2601), app(app(ty_@2, bb), bc)) → new_esEs0(xy230, xy2600, bb, bc)
new_esEs2(Just(xy230), Just(xy2600), app(ty_[], bag)) → new_esEs(xy230, xy2600, bag)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, app(app(app(ty_@3, gh), ha), hb), fb) → new_esEs1(xy231, xy2601, gh, ha, hb)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), app(app(ty_Either, dd), de), cd) → new_esEs3(xy230, xy2600, dd, de)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, app(app(ty_Either, hd), he), fb) → new_esEs3(xy231, xy2601, hd, he)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, fa, app(app(ty_Either, bae), baf)) → new_esEs3(xy232, xy2602, bae, baf)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(xy230, xy2600, beb, bec)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), df, app(app(app(ty_@3, eb), ec), ed)) → new_esEs1(xy231, xy2601, eb, ec, ed)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, fa, app(app(app(ty_@3, baa), bab), bac)) → new_esEs1(xy232, xy2602, baa, bab, bac)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(xy230, xy2600, bdf, bdg, bdh)
new_esEs3(Left(xy230), Left(xy2600), app(app(app(ty_@3, bcd), bce), bcf), bca) → new_esEs1(xy230, xy2600, bcd, bce, bcf)
new_esEs3(Left(xy230), Left(xy2600), app(ty_[], bbh), bca) → new_esEs(xy230, xy2600, bbh)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, fa, app(app(ty_@2, hg), hh)) → new_esEs0(xy232, xy2602, hg, hh)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), df, app(app(ty_Either, ef), eg)) → new_esEs3(xy231, xy2601, ef, eg)
new_esEs2(Just(xy230), Just(xy2600), app(ty_Maybe, bbe)) → new_esEs2(xy230, xy2600, bbe)
new_esEs3(Left(xy230), Left(xy2600), app(app(ty_Either, bch), bda), bca) → new_esEs3(xy230, xy2600, bch, bda)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(ty_@2, fc), fd), fa, fb) → new_esEs0(xy230, xy2600, fc, fd)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), df, app(ty_[], dg)) → new_esEs(xy231, xy2601, dg)
new_esEs(:(xy230, xy231), :(xy2600, xy2601), app(ty_Maybe, bg)) → new_esEs2(xy230, xy2600, bg)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(app(ty_@3, ff), fg), fh), fa, fb) → new_esEs1(xy230, xy2600, ff, fg, fh)
new_esEs3(Left(xy230), Left(xy2600), app(ty_Maybe, bcg), bca) → new_esEs2(xy230, xy2600, bcg)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), df, app(ty_Maybe, ee)) → new_esEs2(xy231, xy2601, ee)
new_esEs(:(xy230, xy231), :(xy2600, xy2601), cb) → new_esEs(xy231, xy2601, cb)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, app(ty_Maybe, hc), fb) → new_esEs2(xy231, xy2601, hc)
new_esEs(:(xy230, xy231), :(xy2600, xy2601), app(app(app(ty_@3, bd), be), bf)) → new_esEs1(xy230, xy2600, bd, be, bf)
new_esEs(:(xy230, xy231), :(xy2600, xy2601), app(app(ty_Either, bh), ca)) → new_esEs3(xy230, xy2600, bh, ca)
new_esEs3(Left(xy230), Left(xy2600), app(app(ty_@2, bcb), bcc), bca) → new_esEs0(xy230, xy2600, bcb, bcc)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(ty_@2, bdd), bde)) → new_esEs0(xy230, xy2600, bdd, bde)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), app(ty_Maybe, dc), cd) → new_esEs2(xy230, xy2600, dc)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(ty_[], eh), fa, fb) → new_esEs(xy230, xy2600, eh)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, fa, app(ty_Maybe, bad)) → new_esEs2(xy232, xy2602, bad)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), app(app(ty_@2, ce), cf), cd) → new_esEs0(xy230, xy2600, ce, cf)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(ty_Maybe, ga), fa, fb) → new_esEs2(xy230, xy2600, ga)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), app(ty_[], cc), cd) → new_esEs(xy230, xy2600, cc)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(ty_Either, gb), gc), fa, fb) → new_esEs3(xy230, xy2600, gb, gc)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(ty_Maybe, bea)) → new_esEs2(xy230, xy2600, bea)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), app(app(app(ty_@3, cg), da), db), cd) → new_esEs1(xy230, xy2600, cg, da, db)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, app(app(ty_@2, gf), gg), fb) → new_esEs0(xy231, xy2601, gf, gg)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, fa, app(ty_[], hf)) → new_esEs(xy232, xy2602, hf)
new_esEs2(Just(xy230), Just(xy2600), app(app(ty_Either, bbf), bbg)) → new_esEs3(xy230, xy2600, bbf, bbg)
new_esEs0(@2(xy230, xy231), @2(xy2600, xy2601), df, app(app(ty_@2, dh), ea)) → new_esEs0(xy231, xy2601, dh, ea)
new_esEs1(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), gd, app(ty_[], ge), fb) → new_esEs(xy231, xy2601, ge)
new_esEs(:(xy230, xy231), :(xy2600, xy2601), app(ty_[], ba)) → new_esEs(xy230, xy2600, ba)
new_esEs2(Just(xy230), Just(xy2600), app(app(ty_@2, bah), bba)) → new_esEs0(xy230, xy2600, bah, bba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf(:(xy220, xy221), :(xy2610, xy2611), ba) → new_isPrefixOf(xy221, xy2611, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf0(xy23, xy22, xy26, :(xy2510, xy2511), ba) → new_isPrefixOf0(xy23, xy22, new_flip(xy26, xy2510, ba), xy2511, ba)

The TRS R consists of the following rules:

new_flip(xy22, xy23, ba) → :(xy23, xy22)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf1(xy22, xy23, :(xy240, xy241), xy25, ba) → new_isPrefixOf1(new_flip(xy22, xy23, ba), xy240, xy241, xy25, ba)

The TRS R consists of the following rules:

new_flip(xy22, xy23, ba) → :(xy23, xy22)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: